es:ES, L:(Id List).
fischer(L)
 (del:.
 fischer-delay(del;L)
  (e:E, j:Id.
  Newround(e)
   (j  L)
   ((j = loc(e)))
   time(the rcv(free message from e to j)) < time(e) + del)) 

latex

Definitions	A, lnk(e), IdLnk, P & Q, x:A. B(x), {T}, SQType(T), "$x", tag(e), P  Q, True, T, Id, , t  T, P  Q, x:A. B(x), False, Newround(e), fischer-delay(del;L)
Lemmas	qadd wf, es-time wf, qless wf, Id sq, Knd wf, Knd sq, kind-f-free, true wf, squash wf, f-free wf, event system wf, fischer wf, rationals wf, fischer-delay wf, es-E wf, f-newround wf, l member wf, es-loc wf, Id wf, not wf, f-free-isrcv, sender-f-free, loc-f-free